\begin{tabbing}
R{-}self{-}interface($R$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$es\_realizer\_ind(\=$R$;\+
\\[0ex]True;
\\[0ex]${\it left}$,${\it right}$,${\it rec}_{1}$,${\it rec}_{2}$.(${\it rec}_{1}$ $\wedge$ ${\it rec}_{2}$);
\\[0ex]${\it loc}$,$T$,$x$,$v$.True;
\\[0ex]${\it loc}$,$T$,$x$,$L$.True;
\\[0ex]${\it lnk}$,${\it tag}$,$L$.True;
\\[0ex]${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$.True;
\\[0ex]${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$.(($\uparrow$isrcv(${\it knd}$))
\\[0ex]$\Rightarrow$ (lnk(${\it knd}$) = $l$)
\\[0ex]$\Rightarrow$ subtype\_rel(fpf{-}cap(${\it dt}$; id{-}deq; tag(${\it knd}$); void); $T$));
\\[0ex]${\it loc}$,${\it ds}$,$a$,$T$,$P$.True;
\\[0ex]${\it loc}$,$k$,$L$.True;
\\[0ex]${\it loc}$,$k$,$L$.True;
\\[0ex]${\it loc}$,$x$,$L$.True)
\-
\end{tabbing}